H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 1.727 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/FiniteMap.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule FiniteMap

((fmToList_LE :: FiniteMap Char a -> Char -> [(Char,a)]) :: FiniteMap Char a -> Char -> [(Char,a)])

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)

instance (Eq a, Eq b) => Eq (FiniteMap b a) where

fmToList_LE :: Ord b => FiniteMap b a -> b -> [(b,a)]

fmToList_LE

fm fr

foldFM_LE (\key elt rest ->(key,elt) : rest) [] fr fm

foldFM_LE :: Ord c => (c -> a -> b -> b) -> b -> c -> FiniteMap c a -> b

foldFM_LE

k z fr EmptyFM

foldFM_LE

k z fr (Branch key elt _ fm_l fm_r)

key <= fr

foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r

otherwise

foldFM_LE k z fr fm_l

module Maybe where

import qualified FiniteMap
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\keyeltrest→(key,elt) : rest

is transformed to

fmToList_LE0 key elt rest = (key,elt) : rest

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule FiniteMap

((fmToList_LE :: FiniteMap Char a -> Char -> [(Char,a)]) :: FiniteMap Char a -> Char -> [(Char,a)])

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)

instance (Eq a, Eq b) => Eq (FiniteMap b a) where

fmToList_LE :: Ord a => FiniteMap a b -> a -> [(a,b)]

fmToList_LE

fm fr

foldFM_LE fmToList_LE0 [] fr fm

fmToList_LE0

key elt rest

(key,elt) : rest

foldFM_LE :: Ord c => (c -> b -> a -> a) -> a -> c -> FiniteMap c b -> a

foldFM_LE

k z fr EmptyFM

foldFM_LE

k z fr (Branch key elt _ fm_l fm_r)

key <= fr

foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r

otherwise

foldFM_LE k z fr fm_l

module Maybe where

import qualified FiniteMap
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule FiniteMap

((fmToList_LE :: FiniteMap Char a -> Char -> [(Char,a)]) :: FiniteMap Char a -> Char -> [(Char,a)])

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a)

instance (Eq a, Eq b) => Eq (FiniteMap b a) where

fmToList_LE :: Ord a => FiniteMap a b -> a -> [(a,b)]

fmToList_LE

fm fr

foldFM_LE fmToList_LE0 [] fr fm

fmToList_LE0

key elt rest

(key,elt) : rest

foldFM_LE :: Ord c => (c -> a -> b -> b) -> b -> c -> FiniteMap c a -> b

foldFM_LE

k z fr EmptyFM

foldFM_LE

k z fr (Branch key elt vw fm_l fm_r)

key <= fr

foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r

otherwise

foldFM_LE k z fr fm_l

module Maybe where

import qualified FiniteMap
import qualified Prelude

Cond Reductions:
The following Function with conditions

foldFM_LE k z fr EmptyFM = z

foldFM_LE k z fr (Branch key elt vw fm_l fm_r)

| key <= fr

= foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r

| otherwise

= foldFM_LE k z fr fm_l

is transformed to

foldFM_LE k z fr EmptyFM = foldFM_LE3 k z fr EmptyFM

foldFM_LE k z fr (Branch key elt vw fm_l fm_r) = foldFM_LE2 k z fr (Branch key elt vw fm_l fm_r)

foldFM_LE0 k z fr key elt vw fm_l fm_r True = foldFM_LE k z fr fm_l

foldFM_LE1 k z fr key elt vw fm_l fm_r True = foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r

foldFM_LE1 k z fr key elt vw fm_l fm_r False = foldFM_LE0 k z fr key elt vw fm_l fm_r otherwise

foldFM_LE2 k z fr (Branch key elt vw fm_l fm_r) = foldFM_LE1 k z fr key elt vw fm_l fm_r (key <= fr)

foldFM_LE3 k z fr EmptyFM = z

foldFM_LE3 wv ww wx wy = foldFM_LE2 wv ww wx wy

The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

mainModule FiniteMap

(fmToList_LE :: FiniteMap Char a -> Char -> [(Char,a)])

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)

instance (Eq a, Eq b) => Eq (FiniteMap b a) where

fmToList_LE :: Ord b => FiniteMap b a -> b -> [(b,a)]

fmToList_LE

fm fr

foldFM_LE fmToList_LE0 [] fr fm

fmToList_LE0

key elt rest

(key,elt) : rest

foldFM_LE :: Ord b => (b -> c -> a -> a) -> a -> b -> FiniteMap b c -> a

foldFM_LE	k z fr EmptyFM	=	foldFM_LE3 k z fr EmptyFM
foldFM_LE	k z fr (Branch key elt vw fm_l fm_r)	=	foldFM_LE2 k z fr (Branch key elt vw fm_l fm_r)

foldFM_LE0

k z fr key elt vw fm_l fm_r True

foldFM_LE k z fr fm_l

foldFM_LE1	k z fr key elt vw fm_l fm_r True	=	foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r
foldFM_LE1	k z fr key elt vw fm_l fm_r False	=	foldFM_LE0 k z fr key elt vw fm_l fm_r otherwise

foldFM_LE2

k z fr (Branch key elt vw fm_l fm_r)

foldFM_LE1 k z fr key elt vw fm_l fm_r (key <= fr)

foldFM_LE3	k z fr EmptyFM	=	z
foldFM_LE3	wv ww wx wy	=	foldFM_LE2 wv ww wx wy

module Maybe where

import qualified FiniteMap
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="fmToList_LE",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="fmToList_LE wz3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="fmToList_LE wz3 wz4",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="foldFM_LE fmToList_LE0 [] wz4 wz3",fontsize=16,color="burlywood",shape="triangle"];861[label="wz3/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];5 -> 861[label="",style="solid", color="burlywood", weight=9];
861 -> 6[label="",style="solid", color="burlywood", weight=3];
862[label="wz3/Branch wz30 wz31 wz32 wz33 wz34",fontsize=10,color="white",style="solid",shape="box"];5 -> 862[label="",style="solid", color="burlywood", weight=9];
862 -> 7[label="",style="solid", color="burlywood", weight=3];
6[label="foldFM_LE fmToList_LE0 [] wz4 EmptyFM",fontsize=16,color="black",shape="box"];6 -> 8[label="",style="solid", color="black", weight=3];
7[label="foldFM_LE fmToList_LE0 [] wz4 (Branch wz30 wz31 wz32 wz33 wz34)",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="foldFM_LE3 fmToList_LE0 [] wz4 EmptyFM",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="foldFM_LE2 fmToList_LE0 [] wz4 (Branch wz30 wz31 wz32 wz33 wz34)",fontsize=16,color="black",shape="box"];9 -> 11[label="",style="solid", color="black", weight=3];
10[label="[]",fontsize=16,color="green",shape="box"];11[label="foldFM_LE1 fmToList_LE0 [] wz4 wz30 wz31 wz32 wz33 wz34 (wz30 <= wz4)",fontsize=16,color="black",shape="box"];11 -> 12[label="",style="solid", color="black", weight=3];
12[label="foldFM_LE1 fmToList_LE0 [] wz4 wz30 wz31 wz32 wz33 wz34 (compare wz30 wz4 /= GT)",fontsize=16,color="black",shape="box"];12 -> 13[label="",style="solid", color="black", weight=3];
13[label="foldFM_LE1 fmToList_LE0 [] wz4 wz30 wz31 wz32 wz33 wz34 (not (compare wz30 wz4 == GT))",fontsize=16,color="black",shape="box"];13 -> 14[label="",style="solid", color="black", weight=3];
14[label="foldFM_LE1 fmToList_LE0 [] wz4 wz30 wz31 wz32 wz33 wz34 (not (primCmpChar wz30 wz4 == GT))",fontsize=16,color="burlywood",shape="box"];863[label="wz30/Char wz300",fontsize=10,color="white",style="solid",shape="box"];14 -> 863[label="",style="solid", color="burlywood", weight=9];
863 -> 15[label="",style="solid", color="burlywood", weight=3];
15[label="foldFM_LE1 fmToList_LE0 [] wz4 (Char wz300) wz31 wz32 wz33 wz34 (not (primCmpChar (Char wz300) wz4 == GT))",fontsize=16,color="burlywood",shape="box"];864[label="wz4/Char wz40",fontsize=10,color="white",style="solid",shape="box"];15 -> 864[label="",style="solid", color="burlywood", weight=9];
864 -> 16[label="",style="solid", color="burlywood", weight=3];
16[label="foldFM_LE1 fmToList_LE0 [] (Char wz40) (Char wz300) wz31 wz32 wz33 wz34 (not (primCmpChar (Char wz300) (Char wz40) == GT))",fontsize=16,color="black",shape="box"];16 -> 17[label="",style="solid", color="black", weight=3];
17[label="foldFM_LE1 fmToList_LE0 [] (Char wz40) (Char wz300) wz31 wz32 wz33 wz34 (not (primCmpNat wz300 wz40 == GT))",fontsize=16,color="burlywood",shape="box"];865[label="wz300/Succ wz3000",fontsize=10,color="white",style="solid",shape="box"];17 -> 865[label="",style="solid", color="burlywood", weight=9];
865 -> 18[label="",style="solid", color="burlywood", weight=3];
866[label="wz300/Zero",fontsize=10,color="white",style="solid",shape="box"];17 -> 866[label="",style="solid", color="burlywood", weight=9];
866 -> 19[label="",style="solid", color="burlywood", weight=3];
18[label="foldFM_LE1 fmToList_LE0 [] (Char wz40) (Char (Succ wz3000)) wz31 wz32 wz33 wz34 (not (primCmpNat (Succ wz3000) wz40 == GT))",fontsize=16,color="burlywood",shape="box"];867[label="wz40/Succ wz400",fontsize=10,color="white",style="solid",shape="box"];18 -> 867[label="",style="solid", color="burlywood", weight=9];
867 -> 20[label="",style="solid", color="burlywood", weight=3];
868[label="wz40/Zero",fontsize=10,color="white",style="solid",shape="box"];18 -> 868[label="",style="solid", color="burlywood", weight=9];
868 -> 21[label="",style="solid", color="burlywood", weight=3];
19[label="foldFM_LE1 fmToList_LE0 [] (Char wz40) (Char Zero) wz31 wz32 wz33 wz34 (not (primCmpNat Zero wz40 == GT))",fontsize=16,color="burlywood",shape="box"];869[label="wz40/Succ wz400",fontsize=10,color="white",style="solid",shape="box"];19 -> 869[label="",style="solid", color="burlywood", weight=9];
869 -> 22[label="",style="solid", color="burlywood", weight=3];
870[label="wz40/Zero",fontsize=10,color="white",style="solid",shape="box"];19 -> 870[label="",style="solid", color="burlywood", weight=9];
870 -> 23[label="",style="solid", color="burlywood", weight=3];
20[label="foldFM_LE1 fmToList_LE0 [] (Char (Succ wz400)) (Char (Succ wz3000)) wz31 wz32 wz33 wz34 (not (primCmpNat (Succ wz3000) (Succ wz400) == GT))",fontsize=16,color="black",shape="box"];20 -> 24[label="",style="solid", color="black", weight=3];
21[label="foldFM_LE1 fmToList_LE0 [] (Char Zero) (Char (Succ wz3000)) wz31 wz32 wz33 wz34 (not (primCmpNat (Succ wz3000) Zero == GT))",fontsize=16,color="black",shape="box"];21 -> 25[label="",style="solid", color="black", weight=3];
22[label="foldFM_LE1 fmToList_LE0 [] (Char (Succ wz400)) (Char Zero) wz31 wz32 wz33 wz34 (not (primCmpNat Zero (Succ wz400) == GT))",fontsize=16,color="black",shape="box"];22 -> 26[label="",style="solid", color="black", weight=3];
23[label="foldFM_LE1 fmToList_LE0 [] (Char Zero) (Char Zero) wz31 wz32 wz33 wz34 (not (primCmpNat Zero Zero == GT))",fontsize=16,color="black",shape="box"];23 -> 27[label="",style="solid", color="black", weight=3];
24 -> 737[label="",style="dashed", color="red", weight=0];
24[label="foldFM_LE1 fmToList_LE0 [] (Char (Succ wz400)) (Char (Succ wz3000)) wz31 wz32 wz33 wz34 (not (primCmpNat wz3000 wz400 == GT))",fontsize=16,color="magenta"];24 -> 738[label="",style="dashed", color="magenta", weight=3];
24 -> 739[label="",style="dashed", color="magenta", weight=3];
24 -> 740[label="",style="dashed", color="magenta", weight=3];
24 -> 741[label="",style="dashed", color="magenta", weight=3];
24 -> 742[label="",style="dashed", color="magenta", weight=3];
24 -> 743[label="",style="dashed", color="magenta", weight=3];
24 -> 744[label="",style="dashed", color="magenta", weight=3];
24 -> 745[label="",style="dashed", color="magenta", weight=3];
24 -> 746[label="",style="dashed", color="magenta", weight=3];
25[label="foldFM_LE1 fmToList_LE0 [] (Char Zero) (Char (Succ wz3000)) wz31 wz32 wz33 wz34 (not (GT == GT))",fontsize=16,color="black",shape="box"];25 -> 30[label="",style="solid", color="black", weight=3];
26[label="foldFM_LE1 fmToList_LE0 [] (Char (Succ wz400)) (Char Zero) wz31 wz32 wz33 wz34 (not (LT == GT))",fontsize=16,color="black",shape="box"];26 -> 31[label="",style="solid", color="black", weight=3];
27[label="foldFM_LE1 fmToList_LE0 [] (Char Zero) (Char Zero) wz31 wz32 wz33 wz34 (not (EQ == GT))",fontsize=16,color="black",shape="box"];27 -> 32[label="",style="solid", color="black", weight=3];
738[label="wz400",fontsize=16,color="green",shape="box"];739[label="wz34",fontsize=16,color="green",shape="box"];740[label="wz400",fontsize=16,color="green",shape="box"];741[label="wz3000",fontsize=16,color="green",shape="box"];742[label="wz31",fontsize=16,color="green",shape="box"];743[label="wz33",fontsize=16,color="green",shape="box"];744[label="wz32",fontsize=16,color="green",shape="box"];745[label="[]",fontsize=16,color="green",shape="box"];746[label="wz3000",fontsize=16,color="green",shape="box"];737[label="foldFM_LE1 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 (not (primCmpNat wz89 wz90 == GT))",fontsize=16,color="burlywood",shape="triangle"];872[label="wz89/Succ wz890",fontsize=10,color="white",style="solid",shape="box"];737 -> 872[label="",style="solid", color="burlywood", weight=9];
872 -> 828[label="",style="solid", color="burlywood", weight=3];
873[label="wz89/Zero",fontsize=10,color="white",style="solid",shape="box"];737 -> 873[label="",style="solid", color="burlywood", weight=9];
873 -> 829[label="",style="solid", color="burlywood", weight=3];
30[label="foldFM_LE1 fmToList_LE0 [] (Char Zero) (Char (Succ wz3000)) wz31 wz32 wz33 wz34 (not True)",fontsize=16,color="black",shape="box"];30 -> 37[label="",style="solid", color="black", weight=3];
31[label="foldFM_LE1 fmToList_LE0 [] (Char (Succ wz400)) (Char Zero) wz31 wz32 wz33 wz34 (not False)",fontsize=16,color="black",shape="box"];31 -> 38[label="",style="solid", color="black", weight=3];
32[label="foldFM_LE1 fmToList_LE0 [] (Char Zero) (Char Zero) wz31 wz32 wz33 wz34 (not False)",fontsize=16,color="black",shape="box"];32 -> 39[label="",style="solid", color="black", weight=3];
828[label="foldFM_LE1 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 (not (primCmpNat (Succ wz890) wz90 == GT))",fontsize=16,color="burlywood",shape="box"];874[label="wz90/Succ wz900",fontsize=10,color="white",style="solid",shape="box"];828 -> 874[label="",style="solid", color="burlywood", weight=9];
874 -> 830[label="",style="solid", color="burlywood", weight=3];
875[label="wz90/Zero",fontsize=10,color="white",style="solid",shape="box"];828 -> 875[label="",style="solid", color="burlywood", weight=9];
875 -> 831[label="",style="solid", color="burlywood", weight=3];
829[label="foldFM_LE1 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 (not (primCmpNat Zero wz90 == GT))",fontsize=16,color="burlywood",shape="box"];876[label="wz90/Succ wz900",fontsize=10,color="white",style="solid",shape="box"];829 -> 876[label="",style="solid", color="burlywood", weight=9];
876 -> 832[label="",style="solid", color="burlywood", weight=3];
877[label="wz90/Zero",fontsize=10,color="white",style="solid",shape="box"];829 -> 877[label="",style="solid", color="burlywood", weight=9];
877 -> 833[label="",style="solid", color="burlywood", weight=3];
37[label="foldFM_LE1 fmToList_LE0 [] (Char Zero) (Char (Succ wz3000)) wz31 wz32 wz33 wz34 False",fontsize=16,color="black",shape="box"];37 -> 44[label="",style="solid", color="black", weight=3];
38[label="foldFM_LE1 fmToList_LE0 [] (Char (Succ wz400)) (Char Zero) wz31 wz32 wz33 wz34 True",fontsize=16,color="black",shape="box"];38 -> 45[label="",style="solid", color="black", weight=3];
39[label="foldFM_LE1 fmToList_LE0 [] (Char Zero) (Char Zero) wz31 wz32 wz33 wz34 True",fontsize=16,color="black",shape="box"];39 -> 46[label="",style="solid", color="black", weight=3];
830[label="foldFM_LE1 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 (not (primCmpNat (Succ wz890) (Succ wz900) == GT))",fontsize=16,color="black",shape="box"];830 -> 834[label="",style="solid", color="black", weight=3];
831[label="foldFM_LE1 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 (not (primCmpNat (Succ wz890) Zero == GT))",fontsize=16,color="black",shape="box"];831 -> 835[label="",style="solid", color="black", weight=3];
832[label="foldFM_LE1 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 (not (primCmpNat Zero (Succ wz900) == GT))",fontsize=16,color="black",shape="box"];832 -> 836[label="",style="solid", color="black", weight=3];
833[label="foldFM_LE1 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 (not (primCmpNat Zero Zero == GT))",fontsize=16,color="black",shape="box"];833 -> 837[label="",style="solid", color="black", weight=3];
44[label="foldFM_LE0 fmToList_LE0 [] (Char Zero) (Char (Succ wz3000)) wz31 wz32 wz33 wz34 otherwise",fontsize=16,color="black",shape="box"];44 -> 52[label="",style="solid", color="black", weight=3];
45 -> 53[label="",style="dashed", color="red", weight=0];
45[label="foldFM_LE fmToList_LE0 (fmToList_LE0 (Char Zero) wz31 (foldFM_LE fmToList_LE0 [] (Char (Succ wz400)) wz33)) (Char (Succ wz400)) wz34",fontsize=16,color="magenta"];45 -> 54[label="",style="dashed", color="magenta", weight=3];
46 -> 55[label="",style="dashed", color="red", weight=0];
46[label="foldFM_LE fmToList_LE0 (fmToList_LE0 (Char Zero) wz31 (foldFM_LE fmToList_LE0 [] (Char Zero) wz33)) (Char Zero) wz34",fontsize=16,color="magenta"];46 -> 56[label="",style="dashed", color="magenta", weight=3];
834 -> 737[label="",style="dashed", color="red", weight=0];
834[label="foldFM_LE1 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 (not (primCmpNat wz890 wz900 == GT))",fontsize=16,color="magenta"];834 -> 838[label="",style="dashed", color="magenta", weight=3];
834 -> 839[label="",style="dashed", color="magenta", weight=3];
835[label="foldFM_LE1 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 (not (GT == GT))",fontsize=16,color="black",shape="box"];835 -> 840[label="",style="solid", color="black", weight=3];
836[label="foldFM_LE1 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 (not (LT == GT))",fontsize=16,color="black",shape="box"];836 -> 841[label="",style="solid", color="black", weight=3];
837[label="foldFM_LE1 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 (not (EQ == GT))",fontsize=16,color="black",shape="box"];837 -> 842[label="",style="solid", color="black", weight=3];
52[label="foldFM_LE0 fmToList_LE0 [] (Char Zero) (Char (Succ wz3000)) wz31 wz32 wz33 wz34 True",fontsize=16,color="black",shape="box"];52 -> 64[label="",style="solid", color="black", weight=3];
54 -> 5[label="",style="dashed", color="red", weight=0];
54[label="foldFM_LE fmToList_LE0 [] (Char (Succ wz400)) wz33",fontsize=16,color="magenta"];54 -> 65[label="",style="dashed", color="magenta", weight=3];
54 -> 66[label="",style="dashed", color="magenta", weight=3];
53[label="foldFM_LE fmToList_LE0 (fmToList_LE0 (Char Zero) wz31 wz5) (Char (Succ wz400)) wz34",fontsize=16,color="burlywood",shape="triangle"];882[label="wz34/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];53 -> 882[label="",style="solid", color="burlywood", weight=9];
882 -> 67[label="",style="solid", color="burlywood", weight=3];
883[label="wz34/Branch wz340 wz341 wz342 wz343 wz344",fontsize=10,color="white",style="solid",shape="box"];53 -> 883[label="",style="solid", color="burlywood", weight=9];
883 -> 68[label="",style="solid", color="burlywood", weight=3];
56 -> 5[label="",style="dashed", color="red", weight=0];
56[label="foldFM_LE fmToList_LE0 [] (Char Zero) wz33",fontsize=16,color="magenta"];56 -> 69[label="",style="dashed", color="magenta", weight=3];
56 -> 70[label="",style="dashed", color="magenta", weight=3];
55[label="foldFM_LE fmToList_LE0 (fmToList_LE0 (Char Zero) wz31 wz6) (Char Zero) wz34",fontsize=16,color="burlywood",shape="triangle"];885[label="wz34/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];55 -> 885[label="",style="solid", color="burlywood", weight=9];
885 -> 71[label="",style="solid", color="burlywood", weight=3];
886[label="wz34/Branch wz340 wz341 wz342 wz343 wz344",fontsize=10,color="white",style="solid",shape="box"];55 -> 886[label="",style="solid", color="burlywood", weight=9];
886 -> 72[label="",style="solid", color="burlywood", weight=3];
838[label="wz900",fontsize=16,color="green",shape="box"];839[label="wz890",fontsize=16,color="green",shape="box"];840[label="foldFM_LE1 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 (not True)",fontsize=16,color="black",shape="box"];840 -> 843[label="",style="solid", color="black", weight=3];
841[label="foldFM_LE1 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 (not False)",fontsize=16,color="black",shape="triangle"];841 -> 844[label="",style="solid", color="black", weight=3];
842 -> 841[label="",style="dashed", color="red", weight=0];
842[label="foldFM_LE1 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 (not False)",fontsize=16,color="magenta"];64 -> 5[label="",style="dashed", color="red", weight=0];
64[label="foldFM_LE fmToList_LE0 [] (Char Zero) wz33",fontsize=16,color="magenta"];64 -> 80[label="",style="dashed", color="magenta", weight=3];
64 -> 81[label="",style="dashed", color="magenta", weight=3];
65[label="wz33",fontsize=16,color="green",shape="box"];66[label="Char (Succ wz400)",fontsize=16,color="green",shape="box"];67[label="foldFM_LE fmToList_LE0 (fmToList_LE0 (Char Zero) wz31 wz5) (Char (Succ wz400)) EmptyFM",fontsize=16,color="black",shape="box"];67 -> 82[label="",style="solid", color="black", weight=3];
68[label="foldFM_LE fmToList_LE0 (fmToList_LE0 (Char Zero) wz31 wz5) (Char (Succ wz400)) (Branch wz340 wz341 wz342 wz343 wz344)",fontsize=16,color="black",shape="box"];68 -> 83[label="",style="solid", color="black", weight=3];
69[label="wz33",fontsize=16,color="green",shape="box"];70[label="Char Zero",fontsize=16,color="green",shape="box"];71[label="foldFM_LE fmToList_LE0 (fmToList_LE0 (Char Zero) wz31 wz6) (Char Zero) EmptyFM",fontsize=16,color="black",shape="box"];71 -> 84[label="",style="solid", color="black", weight=3];
72[label="foldFM_LE fmToList_LE0 (fmToList_LE0 (Char Zero) wz31 wz6) (Char Zero) (Branch wz340 wz341 wz342 wz343 wz344)",fontsize=16,color="black",shape="box"];72 -> 85[label="",style="solid", color="black", weight=3];
843[label="foldFM_LE1 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 False",fontsize=16,color="black",shape="box"];843 -> 845[label="",style="solid", color="black", weight=3];
844[label="foldFM_LE1 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 True",fontsize=16,color="black",shape="box"];844 -> 846[label="",style="solid", color="black", weight=3];
80[label="wz33",fontsize=16,color="green",shape="box"];81[label="Char Zero",fontsize=16,color="green",shape="box"];82[label="foldFM_LE3 fmToList_LE0 (fmToList_LE0 (Char Zero) wz31 wz5) (Char (Succ wz400)) EmptyFM",fontsize=16,color="black",shape="box"];82 -> 96[label="",style="solid", color="black", weight=3];
83[label="foldFM_LE2 fmToList_LE0 (fmToList_LE0 (Char Zero) wz31 wz5) (Char (Succ wz400)) (Branch wz340 wz341 wz342 wz343 wz344)",fontsize=16,color="black",shape="box"];83 -> 97[label="",style="solid", color="black", weight=3];
84[label="foldFM_LE3 fmToList_LE0 (fmToList_LE0 (Char Zero) wz31 wz6) (Char Zero) EmptyFM",fontsize=16,color="black",shape="box"];84 -> 98[label="",style="solid", color="black", weight=3];
85[label="foldFM_LE2 fmToList_LE0 (fmToList_LE0 (Char Zero) wz31 wz6) (Char Zero) (Branch wz340 wz341 wz342 wz343 wz344)",fontsize=16,color="black",shape="box"];85 -> 99[label="",style="solid", color="black", weight=3];
845[label="foldFM_LE0 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 otherwise",fontsize=16,color="black",shape="box"];845 -> 847[label="",style="solid", color="black", weight=3];
846 -> 442[label="",style="dashed", color="red", weight=0];
846[label="foldFM_LE fmToList_LE0 (fmToList_LE0 (Char (Succ wz84)) wz85 (foldFM_LE fmToList_LE0 wz82 (Char (Succ wz83)) wz87)) (Char (Succ wz83)) wz88",fontsize=16,color="magenta"];846 -> 848[label="",style="dashed", color="magenta", weight=3];
846 -> 849[label="",style="dashed", color="magenta", weight=3];
846 -> 850[label="",style="dashed", color="magenta", weight=3];
96[label="fmToList_LE0 (Char Zero) wz31 wz5",fontsize=16,color="black",shape="triangle"];96 -> 116[label="",style="solid", color="black", weight=3];
97 -> 117[label="",style="dashed", color="red", weight=0];
97[label="foldFM_LE1 fmToList_LE0 (fmToList_LE0 (Char Zero) wz31 wz5) (Char (Succ wz400)) wz340 wz341 wz342 wz343 wz344 (wz340 <= Char (Succ wz400))",fontsize=16,color="magenta"];97 -> 118[label="",style="dashed", color="magenta", weight=3];
98 -> 96[label="",style="dashed", color="red", weight=0];
98[label="fmToList_LE0 (Char Zero) wz31 wz6",fontsize=16,color="magenta"];98 -> 119[label="",style="dashed", color="magenta", weight=3];
99 -> 120[label="",style="dashed", color="red", weight=0];
99[label="foldFM_LE1 fmToList_LE0 (fmToList_LE0 (Char Zero) wz31 wz6) (Char Zero) wz340 wz341 wz342 wz343 wz344 (wz340 <= Char Zero)",fontsize=16,color="magenta"];99 -> 121[label="",style="dashed", color="magenta", weight=3];
847[label="foldFM_LE0 fmToList_LE0 wz82 (Char (Succ wz83)) (Char (Succ wz84)) wz85 wz86 wz87 wz88 True",fontsize=16,color="black",shape="box"];847 -> 851[label="",style="solid", color="black", weight=3];
848 -> 852[label="",style="dashed", color="red", weight=0];
848[label="fmToList_LE0 (Char (Succ wz84)) wz85 (foldFM_LE fmToList_LE0 wz82 (Char (Succ wz83)) wz87)",fontsize=16,color="magenta"];848 -> 853[label="",style="dashed", color="magenta", weight=3];
849[label="wz83",fontsize=16,color="green",shape="box"];850[label="wz88",fontsize=16,color="green",shape="box"];442[label="foldFM_LE fmToList_LE0 wz9 (Char (Succ wz400)) wz343",fontsize=16,color="burlywood",shape="triangle"];894[label="wz343/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];442 -> 894[label="",style="solid", color="burlywood", weight=9];
894 -> 522[label="",style="solid", color="burlywood", weight=3];
895[label="wz343/Branch wz3430 wz3431 wz3432 wz3433 wz3434",fontsize=10,color="white",style="solid",shape="box"];442 -> 895[label="",style="solid", color="burlywood", weight=9];
895 -> 523[label="",style="solid", color="burlywood", weight=3];
116[label="(Char Zero,wz31) : wz5",fontsize=16,color="green",shape="box"];118 -> 96[label="",style="dashed", color="red", weight=0];
118[label="fmToList_LE0 (Char Zero) wz31 wz5",fontsize=16,color="magenta"];117[label="foldFM_LE1 fmToList_LE0 wz9 (Char (Succ wz400)) wz340 wz341 wz342 wz343 wz344 (wz340 <= Char (Succ wz400))",fontsize=16,color="black",shape="triangle"];117 -> 135[label="",style="solid", color="black", weight=3];
119[label="wz6",fontsize=16,color="green",shape="box"];121 -> 96[label="",style="dashed", color="red", weight=0];
121[label="fmToList_LE0 (Char Zero) wz31 wz6",fontsize=16,color="magenta"];121 -> 136[label="",style="dashed", color="magenta", weight=3];
120[label="foldFM_LE1 fmToList_LE0 wz10 (Char Zero) wz340 wz341 wz342 wz343 wz344 (wz340 <= Char Zero)",fontsize=16,color="black",shape="triangle"];120 -> 137[label="",style="solid", color="black", weight=3];
851 -> 442[label="",style="dashed", color="red", weight=0];
851[label="foldFM_LE fmToList_LE0 wz82 (Char (Succ wz83)) wz87",fontsize=16,color="magenta"];851 -> 854[label="",style="dashed", color="magenta", weight=3];
851 -> 855[label="",style="dashed", color="magenta", weight=3];
851 -> 856[label="",style="dashed", color="magenta", weight=3];
853 -> 442[label="",style="dashed", color="red", weight=0];
853[label="foldFM_LE fmToList_LE0 wz82 (Char (Succ wz83)) wz87",fontsize=16,color="magenta"];853 -> 857[label="",style="dashed", color="magenta", weight=3];
853 -> 858[label="",style="dashed", color="magenta", weight=3];
853 -> 859[label="",style="dashed", color="magenta", weight=3];
852[label="fmToList_LE0 (Char (Succ wz84)) wz85 wz91",fontsize=16,color="black",shape="triangle"];852 -> 860[label="",style="solid", color="black", weight=3];
522[label="foldFM_LE fmToList_LE0 wz9 (Char (Succ wz400)) EmptyFM",fontsize=16,color="black",shape="box"];522 -> 538[label="",style="solid", color="black", weight=3];
523[label="foldFM_LE fmToList_LE0 wz9 (Char (Succ wz400)) (Branch wz3430 wz3431 wz3432 wz3433 wz3434)",fontsize=16,color="black",shape="box"];523 -> 539[label="",style="solid", color="black", weight=3];
135[label="foldFM_LE1 fmToList_LE0 wz9 (Char (Succ wz400)) wz340 wz341 wz342 wz343 wz344 (compare wz340 (Char (Succ wz400)) /= GT)",fontsize=16,color="black",shape="box"];135 -> 152[label="",style="solid", color="black", weight=3];
136[label="wz6",fontsize=16,color="green",shape="box"];137[label="foldFM_LE1 fmToList_LE0 wz10 (Char Zero) wz340 wz341 wz342 wz343 wz344 (compare wz340 (Char Zero) /= GT)",fontsize=16,color="black",shape="box"];137 -> 153[label="",style="solid", color="black", weight=3];
854[label="wz82",fontsize=16,color="green",shape="box"];855[label="wz83",fontsize=16,color="green",shape="box"];856[label="wz87",fontsize=16,color="green",shape="box"];857[label="wz82",fontsize=16,color="green",shape="box"];858[label="wz83",fontsize=16,color="green",shape="box"];859[label="wz87",fontsize=16,color="green",shape="box"];860[label="(Char (Succ wz84),wz85) : wz91",fontsize=16,color="green",shape="box"];538[label="foldFM_LE3 fmToList_LE0 wz9 (Char (Succ wz400)) EmptyFM",fontsize=16,color="black",shape="box"];538 -> 558[label="",style="solid", color="black", weight=3];
539[label="foldFM_LE2 fmToList_LE0 wz9 (Char (Succ wz400)) (Branch wz3430 wz3431 wz3432 wz3433 wz3434)",fontsize=16,color="black",shape="box"];539 -> 559[label="",style="solid", color="black", weight=3];
152[label="foldFM_LE1 fmToList_LE0 wz9 (Char (Succ wz400)) wz340 wz341 wz342 wz343 wz344 (not (compare wz340 (Char (Succ wz400)) == GT))",fontsize=16,color="black",shape="box"];152 -> 176[label="",style="solid", color="black", weight=3];
153[label="foldFM_LE1 fmToList_LE0 wz10 (Char Zero) wz340 wz341 wz342 wz343 wz344 (not (compare wz340 (Char Zero) == GT))",fontsize=16,color="black",shape="box"];153 -> 177[label="",style="solid", color="black", weight=3];
558[label="wz9",fontsize=16,color="green",shape="box"];559 -> 117[label="",style="dashed", color="red", weight=0];
559[label="foldFM_LE1 fmToList_LE0 wz9 (Char (Succ wz400)) wz3430 wz3431 wz3432 wz3433 wz3434 (wz3430 <= Char (Succ wz400))",fontsize=16,color="magenta"];559 -> 580[label="",style="dashed", color="magenta", weight=3];
559 -> 581[label="",style="dashed", color="magenta", weight=3];
559 -> 582[label="",style="dashed", color="magenta", weight=3];
559 -> 583[label="",style="dashed", color="magenta", weight=3];
559 -> 584[label="",style="dashed", color="magenta", weight=3];
176[label="foldFM_LE1 fmToList_LE0 wz9 (Char (Succ wz400)) wz340 wz341 wz342 wz343 wz344 (not (primCmpChar wz340 (Char (Succ wz400)) == GT))",fontsize=16,color="burlywood",shape="box"];901[label="wz340/Char wz3400",fontsize=10,color="white",style="solid",shape="box"];176 -> 901[label="",style="solid", color="burlywood", weight=9];
901 -> 192[label="",style="solid", color="burlywood", weight=3];
177[label="foldFM_LE1 fmToList_LE0 wz10 (Char Zero) wz340 wz341 wz342 wz343 wz344 (not (primCmpChar wz340 (Char Zero) == GT))",fontsize=16,color="burlywood",shape="box"];902[label="wz340/Char wz3400",fontsize=10,color="white",style="solid",shape="box"];177 -> 902[label="",style="solid", color="burlywood", weight=9];
902 -> 193[label="",style="solid", color="burlywood", weight=3];
580[label="wz3434",fontsize=16,color="green",shape="box"];581[label="wz3431",fontsize=16,color="green",shape="box"];582[label="wz3433",fontsize=16,color="green",shape="box"];583[label="wz3432",fontsize=16,color="green",shape="box"];584[label="wz3430",fontsize=16,color="green",shape="box"];192[label="foldFM_LE1 fmToList_LE0 wz9 (Char (Succ wz400)) (Char wz3400) wz341 wz342 wz343 wz344 (not (primCmpChar (Char wz3400) (Char (Succ wz400)) == GT))",fontsize=16,color="black",shape="box"];192 -> 208[label="",style="solid", color="black", weight=3];
193[label="foldFM_LE1 fmToList_LE0 wz10 (Char Zero) (Char wz3400) wz341 wz342 wz343 wz344 (not (primCmpChar (Char wz3400) (Char Zero) == GT))",fontsize=16,color="black",shape="box"];193 -> 209[label="",style="solid", color="black", weight=3];
208[label="foldFM_LE1 fmToList_LE0 wz9 (Char (Succ wz400)) (Char wz3400) wz341 wz342 wz343 wz344 (not (primCmpNat wz3400 (Succ wz400) == GT))",fontsize=16,color="burlywood",shape="box"];903[label="wz3400/Succ wz34000",fontsize=10,color="white",style="solid",shape="box"];208 -> 903[label="",style="solid", color="burlywood", weight=9];
903 -> 232[label="",style="solid", color="burlywood", weight=3];
904[label="wz3400/Zero",fontsize=10,color="white",style="solid",shape="box"];208 -> 904[label="",style="solid", color="burlywood", weight=9];
904 -> 233[label="",style="solid", color="burlywood", weight=3];
209[label="foldFM_LE1 fmToList_LE0 wz10 (Char Zero) (Char wz3400) wz341 wz342 wz343 wz344 (not (primCmpNat wz3400 Zero == GT))",fontsize=16,color="burlywood",shape="box"];905[label="wz3400/Succ wz34000",fontsize=10,color="white",style="solid",shape="box"];209 -> 905[label="",style="solid", color="burlywood", weight=9];
905 -> 234[label="",style="solid", color="burlywood", weight=3];
906[label="wz3400/Zero",fontsize=10,color="white",style="solid",shape="box"];209 -> 906[label="",style="solid", color="burlywood", weight=9];
906 -> 235[label="",style="solid", color="burlywood", weight=3];
232[label="foldFM_LE1 fmToList_LE0 wz9 (Char (Succ wz400)) (Char (Succ wz34000)) wz341 wz342 wz343 wz344 (not (primCmpNat (Succ wz34000) (Succ wz400) == GT))",fontsize=16,color="black",shape="box"];232 -> 250[label="",style="solid", color="black", weight=3];
233[label="foldFM_LE1 fmToList_LE0 wz9 (Char (Succ wz400)) (Char Zero) wz341 wz342 wz343 wz344 (not (primCmpNat Zero (Succ wz400) == GT))",fontsize=16,color="black",shape="box"];233 -> 251[label="",style="solid", color="black", weight=3];
234[label="foldFM_LE1 fmToList_LE0 wz10 (Char Zero) (Char (Succ wz34000)) wz341 wz342 wz343 wz344 (not (primCmpNat (Succ wz34000) Zero == GT))",fontsize=16,color="black",shape="box"];234 -> 252[label="",style="solid", color="black", weight=3];
235[label="foldFM_LE1 fmToList_LE0 wz10 (Char Zero) (Char Zero) wz341 wz342 wz343 wz344 (not (primCmpNat Zero Zero == GT))",fontsize=16,color="black",shape="box"];235 -> 253[label="",style="solid", color="black", weight=3];
250 -> 737[label="",style="dashed", color="red", weight=0];
250[label="foldFM_LE1 fmToList_LE0 wz9 (Char (Succ wz400)) (Char (Succ wz34000)) wz341 wz342 wz343 wz344 (not (primCmpNat wz34000 wz400 == GT))",fontsize=16,color="magenta"];250 -> 765[label="",style="dashed", color="magenta", weight=3];
250 -> 766[label="",style="dashed", color="magenta", weight=3];
250 -> 767[label="",style="dashed", color="magenta", weight=3];
250 -> 768[label="",style="dashed", color="magenta", weight=3];
250 -> 769[label="",style="dashed", color="magenta", weight=3];
250 -> 770[label="",style="dashed", color="magenta", weight=3];
250 -> 771[label="",style="dashed", color="magenta", weight=3];
250 -> 772[label="",style="dashed", color="magenta", weight=3];
250 -> 773[label="",style="dashed", color="magenta", weight=3];
251[label="foldFM_LE1 fmToList_LE0 wz9 (Char (Succ wz400)) (Char Zero) wz341 wz342 wz343 wz344 (not (LT == GT))",fontsize=16,color="black",shape="box"];251 -> 286[label="",style="solid", color="black", weight=3];
252[label="foldFM_LE1 fmToList_LE0 wz10 (Char Zero) (Char (Succ wz34000)) wz341 wz342 wz343 wz344 (not (GT == GT))",fontsize=16,color="black",shape="box"];252 -> 287[label="",style="solid", color="black", weight=3];
253[label="foldFM_LE1 fmToList_LE0 wz10 (Char Zero) (Char Zero) wz341 wz342 wz343 wz344 (not (EQ == GT))",fontsize=16,color="black",shape="box"];253 -> 288[label="",style="solid", color="black", weight=3];
765[label="wz400",fontsize=16,color="green",shape="box"];766[label="wz344",fontsize=16,color="green",shape="box"];767[label="wz400",fontsize=16,color="green",shape="box"];768[label="wz34000",fontsize=16,color="green",shape="box"];769[label="wz341",fontsize=16,color="green",shape="box"];770[label="wz343",fontsize=16,color="green",shape="box"];771[label="wz342",fontsize=16,color="green",shape="box"];772[label="wz9",fontsize=16,color="green",shape="box"];773[label="wz34000",fontsize=16,color="green",shape="box"];286[label="foldFM_LE1 fmToList_LE0 wz9 (Char (Succ wz400)) (Char Zero) wz341 wz342 wz343 wz344 (not False)",fontsize=16,color="black",shape="box"];286 -> 343[label="",style="solid", color="black", weight=3];
287[label="foldFM_LE1 fmToList_LE0 wz10 (Char Zero) (Char (Succ wz34000)) wz341 wz342 wz343 wz344 (not True)",fontsize=16,color="black",shape="box"];287 -> 344[label="",style="solid", color="black", weight=3];
288[label="foldFM_LE1 fmToList_LE0 wz10 (Char Zero) (Char Zero) wz341 wz342 wz343 wz344 (not False)",fontsize=16,color="black",shape="box"];288 -> 345[label="",style="solid", color="black", weight=3];
343[label="foldFM_LE1 fmToList_LE0 wz9 (Char (Succ wz400)) (Char Zero) wz341 wz342 wz343 wz344 True",fontsize=16,color="black",shape="box"];343 -> 361[label="",style="solid", color="black", weight=3];
344[label="foldFM_LE1 fmToList_LE0 wz10 (Char Zero) (Char (Succ wz34000)) wz341 wz342 wz343 wz344 False",fontsize=16,color="black",shape="box"];344 -> 362[label="",style="solid", color="black", weight=3];
345[label="foldFM_LE1 fmToList_LE0 wz10 (Char Zero) (Char Zero) wz341 wz342 wz343 wz344 True",fontsize=16,color="black",shape="box"];345 -> 363[label="",style="solid", color="black", weight=3];
361 -> 53[label="",style="dashed", color="red", weight=0];
361[label="foldFM_LE fmToList_LE0 (fmToList_LE0 (Char Zero) wz341 (foldFM_LE fmToList_LE0 wz9 (Char (Succ wz400)) wz343)) (Char (Succ wz400)) wz344",fontsize=16,color="magenta"];361 -> 441[label="",style="dashed", color="magenta", weight=3];
361 -> 442[label="",style="dashed", color="magenta", weight=3];
361 -> 443[label="",style="dashed", color="magenta", weight=3];
362[label="foldFM_LE0 fmToList_LE0 wz10 (Char Zero) (Char (Succ wz34000)) wz341 wz342 wz343 wz344 otherwise",fontsize=16,color="black",shape="box"];362 -> 444[label="",style="solid", color="black", weight=3];
363 -> 55[label="",style="dashed", color="red", weight=0];
363[label="foldFM_LE fmToList_LE0 (fmToList_LE0 (Char Zero) wz341 (foldFM_LE fmToList_LE0 wz10 (Char Zero) wz343)) (Char Zero) wz344",fontsize=16,color="magenta"];363 -> 445[label="",style="dashed", color="magenta", weight=3];
363 -> 446[label="",style="dashed", color="magenta", weight=3];
363 -> 447[label="",style="dashed", color="magenta", weight=3];
441[label="wz344",fontsize=16,color="green",shape="box"];443[label="wz341",fontsize=16,color="green",shape="box"];444[label="foldFM_LE0 fmToList_LE0 wz10 (Char Zero) (Char (Succ wz34000)) wz341 wz342 wz343 wz344 True",fontsize=16,color="black",shape="box"];444 -> 524[label="",style="solid", color="black", weight=3];
445[label="wz344",fontsize=16,color="green",shape="box"];446[label="foldFM_LE fmToList_LE0 wz10 (Char Zero) wz343",fontsize=16,color="burlywood",shape="triangle"];910[label="wz343/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];446 -> 910[label="",style="solid", color="burlywood", weight=9];
910 -> 525[label="",style="solid", color="burlywood", weight=3];
911[label="wz343/Branch wz3430 wz3431 wz3432 wz3433 wz3434",fontsize=10,color="white",style="solid",shape="box"];446 -> 911[label="",style="solid", color="burlywood", weight=9];
911 -> 526[label="",style="solid", color="burlywood", weight=3];
447[label="wz341",fontsize=16,color="green",shape="box"];524 -> 446[label="",style="dashed", color="red", weight=0];
524[label="foldFM_LE fmToList_LE0 wz10 (Char Zero) wz343",fontsize=16,color="magenta"];525[label="foldFM_LE fmToList_LE0 wz10 (Char Zero) EmptyFM",fontsize=16,color="black",shape="box"];525 -> 540[label="",style="solid", color="black", weight=3];
526[label="foldFM_LE fmToList_LE0 wz10 (Char Zero) (Branch wz3430 wz3431 wz3432 wz3433 wz3434)",fontsize=16,color="black",shape="box"];526 -> 541[label="",style="solid", color="black", weight=3];
540[label="foldFM_LE3 fmToList_LE0 wz10 (Char Zero) EmptyFM",fontsize=16,color="black",shape="box"];540 -> 560[label="",style="solid", color="black", weight=3];
541[label="foldFM_LE2 fmToList_LE0 wz10 (Char Zero) (Branch wz3430 wz3431 wz3432 wz3433 wz3434)",fontsize=16,color="black",shape="box"];541 -> 561[label="",style="solid", color="black", weight=3];
560[label="wz10",fontsize=16,color="green",shape="box"];561 -> 120[label="",style="dashed", color="red", weight=0];
561[label="foldFM_LE1 fmToList_LE0 wz10 (Char Zero) wz3430 wz3431 wz3432 wz3433 wz3434 (wz3430 <= Char Zero)",fontsize=16,color="magenta"];561 -> 585[label="",style="dashed", color="magenta", weight=3];
561 -> 586[label="",style="dashed", color="magenta", weight=3];
561 -> 587[label="",style="dashed", color="magenta", weight=3];
561 -> 588[label="",style="dashed", color="magenta", weight=3];
561 -> 589[label="",style="dashed", color="magenta", weight=3];
585[label="wz3434",fontsize=16,color="green",shape="box"];586[label="wz3431",fontsize=16,color="green",shape="box"];587[label="wz3433",fontsize=16,color="green",shape="box"];588[label="wz3432",fontsize=16,color="green",shape="box"];589[label="wz3430",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_LE(wz10, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), h) → new_foldFM_LE1(wz10, wz3430, wz3431, wz3432, wz3433, wz3434, h)
new_foldFM_LE1(wz10, Char(Zero), wz341, wz342, wz343, wz344, h) → new_foldFM_LE0(wz341, new_foldFM_LE2(wz10, wz343, h), wz344, h)
new_foldFM_LE1(wz10, Char(Succ(wz34000)), wz341, wz342, wz343, wz344, h) → new_foldFM_LE(wz10, wz343, h)
new_foldFM_LE1(wz10, Char(Zero), wz341, wz342, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), wz344, h) → new_foldFM_LE1(wz10, wz3430, wz3431, wz3432, wz3433, wz3434, h)
new_foldFM_LE0(wz31, wz6, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE1(new_fmToList_LE0(wz31, wz6, h), wz340, wz341, wz342, wz343, wz344, h)

The TRS R consists of the following rules:

new_foldFM_LE10(wz10, Char(Zero), wz341, wz342, wz343, wz344, h) → new_foldFM_LE3(wz341, new_foldFM_LE2(wz10, wz343, h), wz344, h)
new_fmToList_LE0(wz31, wz5, h) → :(@2(Char(Zero), wz31), wz5)
new_foldFM_LE2(wz10, EmptyFM, h) → wz10
new_foldFM_LE3(wz31, wz6, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE10(new_fmToList_LE0(wz31, wz6, h), wz340, wz341, wz342, wz343, wz344, h)
new_foldFM_LE3(wz31, wz6, EmptyFM, h) → new_fmToList_LE0(wz31, wz6, h)
new_foldFM_LE2(wz10, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), h) → new_foldFM_LE10(wz10, wz3430, wz3431, wz3432, wz3433, wz3434, h)
new_foldFM_LE10(wz10, Char(Succ(wz34000)), wz341, wz342, wz343, wz344, h) → new_foldFM_LE2(wz10, wz343, h)

The set Q consists of the following terms:

new_foldFM_LE10(x0, Char(Zero), x1, x2, x3, x4, x5)
new_foldFM_LE3(x0, x1, EmptyFM, x2)
new_foldFM_LE2(x0, EmptyFM, x1)
new_fmToList_LE0(x0, x1, x2)
new_foldFM_LE3(x0, x1, Branch(x2, x3, x4, x5, x6), x7)
new_foldFM_LE2(x0, Branch(x1, x2, x3, x4, x5), x6)
new_foldFM_LE10(x0, Char(Succ(x1)), x2, x3, x4, x5, x6)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_foldFM_LE1(wz10, Char(Succ(wz34000)), wz341, wz342, wz343, wz344, h) → new_foldFM_LE(wz10, wz343, h)
The graph contains the following edges 1 >= 1, 5 >= 2, 7 >= 3
new_foldFM_LE1(wz10, Char(Zero), wz341, wz342, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), wz344, h) → new_foldFM_LE1(wz10, wz3430, wz3431, wz3432, wz3433, wz3434, h)
The graph contains the following edges 1 >= 1, 5 > 2, 5 > 3, 5 > 4, 5 > 5, 5 > 6, 7 >= 7
new_foldFM_LE1(wz10, Char(Zero), wz341, wz342, wz343, wz344, h) → new_foldFM_LE0(wz341, new_foldFM_LE2(wz10, wz343, h), wz344, h)
The graph contains the following edges 3 >= 1, 6 >= 3, 7 >= 4
new_foldFM_LE0(wz31, wz6, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE1(new_fmToList_LE0(wz31, wz6, h), wz340, wz341, wz342, wz343, wz344, h)
The graph contains the following edges 3 > 2, 3 > 3, 3 > 4, 3 > 5, 3 > 6, 4 >= 7
new_foldFM_LE(wz10, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), h) → new_foldFM_LE1(wz10, wz3430, wz3431, wz3432, wz3433, wz3434, h)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 2 > 4, 2 > 5, 2 > 6, 3 >= 7

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_LE11(wz82, wz83, wz84, wz85, wz86, wz87, wz88, Zero, Zero, h) → new_foldFM_LE12(wz82, wz83, wz84, wz85, wz86, wz87, wz88, h)
new_foldFM_LE12(wz82, wz83, wz84, wz85, wz86, wz87, wz88, h) → new_foldFM_LE4(wz82, wz83, wz87, h)
new_foldFM_LE13(wz9, wz400, Char(Succ(wz34000)), wz341, wz342, wz343, wz344, ba) → new_foldFM_LE11(wz9, wz400, wz34000, wz341, wz342, wz343, wz344, wz34000, wz400, ba)
new_foldFM_LE11(wz82, wz83, wz84, wz85, wz86, wz87, wz88, Succ(wz890), Succ(wz900), h) → new_foldFM_LE11(wz82, wz83, wz84, wz85, wz86, wz87, wz88, wz890, wz900, h)
new_foldFM_LE11(wz82, wz83, wz84, wz85, wz86, wz87, wz88, Succ(wz890), Zero, h) → new_foldFM_LE4(wz82, wz83, wz87, h)
new_foldFM_LE11(wz82, wz83, wz84, wz85, wz86, wz87, wz88, Zero, Succ(wz900), h) → new_foldFM_LE4(wz82, wz83, wz87, h)
new_foldFM_LE11(wz82, wz83, wz84, wz85, wz86, wz87, wz88, Zero, Succ(wz900), h) → new_foldFM_LE4(new_fmToList_LE00(wz84, wz85, new_foldFM_LE5(wz82, wz83, wz87, h), h), wz83, wz88, h)
new_foldFM_LE4(wz9, wz400, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), ba) → new_foldFM_LE13(wz9, wz400, wz3430, wz3431, wz3432, wz3433, wz3434, ba)
new_foldFM_LE13(wz9, wz400, Char(Zero), wz341, wz342, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), wz344, ba) → new_foldFM_LE13(wz9, wz400, wz3430, wz3431, wz3432, wz3433, wz3434, ba)
new_foldFM_LE13(wz9, wz400, Char(Zero), wz341, wz342, wz343, wz344, ba) → new_foldFM_LE6(wz341, new_foldFM_LE5(wz9, wz400, wz343, ba), wz400, wz344, ba)
new_foldFM_LE12(wz82, wz83, wz84, wz85, wz86, wz87, wz88, h) → new_foldFM_LE4(new_fmToList_LE00(wz84, wz85, new_foldFM_LE5(wz82, wz83, wz87, h), h), wz83, wz88, h)
new_foldFM_LE6(wz31, wz5, wz400, Branch(wz340, wz341, wz342, wz343, wz344), ba) → new_foldFM_LE13(new_fmToList_LE0(wz31, wz5, ba), wz400, wz340, wz341, wz342, wz343, wz344, ba)

The TRS R consists of the following rules:

new_foldFM_LE14(wz9, wz400, Char(Succ(wz34000)), wz341, wz342, wz343, wz344, ba) → new_foldFM_LE16(wz9, wz400, wz34000, wz341, wz342, wz343, wz344, wz34000, wz400, ba)
new_foldFM_LE7(wz31, wz5, wz400, EmptyFM, ba) → new_fmToList_LE0(wz31, wz5, ba)
new_foldFM_LE15(wz82, wz83, wz84, wz85, wz86, wz87, wz88, h) → new_foldFM_LE5(new_fmToList_LE00(wz84, wz85, new_foldFM_LE5(wz82, wz83, wz87, h), h), wz83, wz88, h)
new_foldFM_LE5(wz9, wz400, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), ba) → new_foldFM_LE14(wz9, wz400, wz3430, wz3431, wz3432, wz3433, wz3434, ba)
new_foldFM_LE16(wz82, wz83, wz84, wz85, wz86, wz87, wz88, Succ(wz890), Succ(wz900), h) → new_foldFM_LE16(wz82, wz83, wz84, wz85, wz86, wz87, wz88, wz890, wz900, h)
new_foldFM_LE16(wz82, wz83, wz84, wz85, wz86, wz87, wz88, Zero, Zero, h) → new_foldFM_LE15(wz82, wz83, wz84, wz85, wz86, wz87, wz88, h)
new_foldFM_LE16(wz82, wz83, wz84, wz85, wz86, wz87, wz88, Succ(wz890), Zero, h) → new_foldFM_LE5(wz82, wz83, wz87, h)
new_fmToList_LE00(wz84, wz85, wz91, h) → :(@2(Char(Succ(wz84)), wz85), wz91)
new_foldFM_LE7(wz31, wz5, wz400, Branch(wz340, wz341, wz342, wz343, wz344), ba) → new_foldFM_LE14(new_fmToList_LE0(wz31, wz5, ba), wz400, wz340, wz341, wz342, wz343, wz344, ba)
new_foldFM_LE16(wz82, wz83, wz84, wz85, wz86, wz87, wz88, Zero, Succ(wz900), h) → new_foldFM_LE15(wz82, wz83, wz84, wz85, wz86, wz87, wz88, h)
new_fmToList_LE0(wz31, wz5, ba) → :(@2(Char(Zero), wz31), wz5)
new_foldFM_LE14(wz9, wz400, Char(Zero), wz341, wz342, wz343, wz344, ba) → new_foldFM_LE7(wz341, new_foldFM_LE5(wz9, wz400, wz343, ba), wz400, wz344, ba)
new_foldFM_LE5(wz9, wz400, EmptyFM, ba) → wz9

The set Q consists of the following terms:

new_foldFM_LE7(x0, x1, x2, EmptyFM, x3)
new_foldFM_LE14(x0, x1, Char(Zero), x2, x3, x4, x5, x6)
new_foldFM_LE7(x0, x1, x2, Branch(x3, x4, x5, x6, x7), x8)
new_fmToList_LE0(x0, x1, x2)
new_foldFM_LE16(x0, x1, x2, x3, x4, x5, x6, Succ(x7), Zero, x8)
new_foldFM_LE16(x0, x1, x2, x3, x4, x5, x6, Zero, Zero, x7)
new_foldFM_LE16(x0, x1, x2, x3, x4, x5, x6, Zero, Succ(x7), x8)
new_foldFM_LE14(x0, x1, Char(Succ(x2)), x3, x4, x5, x6, x7)
new_foldFM_LE15(x0, x1, x2, x3, x4, x5, x6, x7)
new_foldFM_LE5(x0, x1, Branch(x2, x3, x4, x5, x6), x7)
new_foldFM_LE5(x0, x1, EmptyFM, x2)
new_foldFM_LE16(x0, x1, x2, x3, x4, x5, x6, Succ(x7), Succ(x8), x9)
new_fmToList_LE00(x0, x1, x2, x3)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_foldFM_LE4(wz9, wz400, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), ba) → new_foldFM_LE13(wz9, wz400, wz3430, wz3431, wz3432, wz3433, wz3434, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4, 3 > 5, 3 > 6, 3 > 7, 4 >= 8
new_foldFM_LE11(wz82, wz83, wz84, wz85, wz86, wz87, wz88, Zero, Zero, h) → new_foldFM_LE12(wz82, wz83, wz84, wz85, wz86, wz87, wz88, h)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7, 10 >= 8
new_foldFM_LE11(wz82, wz83, wz84, wz85, wz86, wz87, wz88, Succ(wz890), Succ(wz900), h) → new_foldFM_LE11(wz82, wz83, wz84, wz85, wz86, wz87, wz88, wz890, wz900, h)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7, 8 > 8, 9 > 9, 10 >= 10
new_foldFM_LE13(wz9, wz400, Char(Succ(wz34000)), wz341, wz342, wz343, wz344, ba) → new_foldFM_LE11(wz9, wz400, wz34000, wz341, wz342, wz343, wz344, wz34000, wz400, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7, 3 > 8, 2 >= 9, 8 >= 10
new_foldFM_LE13(wz9, wz400, Char(Zero), wz341, wz342, wz343, wz344, ba) → new_foldFM_LE6(wz341, new_foldFM_LE5(wz9, wz400, wz343, ba), wz400, wz344, ba)
The graph contains the following edges 4 >= 1, 2 >= 3, 7 >= 4, 8 >= 5
new_foldFM_LE13(wz9, wz400, Char(Zero), wz341, wz342, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), wz344, ba) → new_foldFM_LE13(wz9, wz400, wz3430, wz3431, wz3432, wz3433, wz3434, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 6 > 3, 6 > 4, 6 > 5, 6 > 6, 6 > 7, 8 >= 8
new_foldFM_LE6(wz31, wz5, wz400, Branch(wz340, wz341, wz342, wz343, wz344), ba) → new_foldFM_LE13(new_fmToList_LE0(wz31, wz5, ba), wz400, wz340, wz341, wz342, wz343, wz344, ba)
The graph contains the following edges 3 >= 2, 4 > 3, 4 > 4, 4 > 5, 4 > 6, 4 > 7, 5 >= 8
new_foldFM_LE12(wz82, wz83, wz84, wz85, wz86, wz87, wz88, h) → new_foldFM_LE4(wz82, wz83, wz87, h)
The graph contains the following edges 1 >= 1, 2 >= 2, 6 >= 3, 8 >= 4
new_foldFM_LE12(wz82, wz83, wz84, wz85, wz86, wz87, wz88, h) → new_foldFM_LE4(new_fmToList_LE00(wz84, wz85, new_foldFM_LE5(wz82, wz83, wz87, h), h), wz83, wz88, h)
The graph contains the following edges 2 >= 2, 7 >= 3, 8 >= 4
new_foldFM_LE11(wz82, wz83, wz84, wz85, wz86, wz87, wz88, Zero, Succ(wz900), h) → new_foldFM_LE4(wz82, wz83, wz87, h)
The graph contains the following edges 1 >= 1, 2 >= 2, 6 >= 3, 10 >= 4
new_foldFM_LE11(wz82, wz83, wz84, wz85, wz86, wz87, wz88, Succ(wz890), Zero, h) → new_foldFM_LE4(wz82, wz83, wz87, h)
The graph contains the following edges 1 >= 1, 2 >= 2, 6 >= 3, 10 >= 4
new_foldFM_LE11(wz82, wz83, wz84, wz85, wz86, wz87, wz88, Zero, Succ(wz900), h) → new_foldFM_LE4(new_fmToList_LE00(wz84, wz85, new_foldFM_LE5(wz82, wz83, wz87, h), h), wz83, wz88, h)
The graph contains the following edges 2 >= 2, 7 >= 3, 10 >= 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_LE8(Char(Zero), Branch(Char(Succ(wz3000)), wz31, wz32, wz33, wz34), h) → new_foldFM_LE8(Char(Zero), wz33, h)
new_foldFM_LE8(Char(Zero), Branch(Char(Zero), wz31, wz32, wz33, wz34), h) → new_foldFM_LE8(Char(Zero), wz33, h)
new_foldFM_LE8(Char(Succ(wz400)), Branch(Char(Zero), wz31, wz32, wz33, wz34), h) → new_foldFM_LE8(Char(Succ(wz400)), wz33, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                          ↳ QDPSizeChangeProof

                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_LE8(Char(Succ(wz400)), Branch(Char(Zero), wz31, wz32, wz33, wz34), h) → new_foldFM_LE8(Char(Succ(wz400)), wz33, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_foldFM_LE8(Char(Succ(wz400)), Branch(Char(Zero), wz31, wz32, wz33, wz34), h) → new_foldFM_LE8(Char(Succ(wz400)), wz33, h)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_LE8(Char(Zero), Branch(Char(Succ(wz3000)), wz31, wz32, wz33, wz34), h) → new_foldFM_LE8(Char(Zero), wz33, h)
new_foldFM_LE8(Char(Zero), Branch(Char(Zero), wz31, wz32, wz33, wz34), h) → new_foldFM_LE8(Char(Zero), wz33, h)

From the DPs we obtained the following set of size-change graphs:

new_foldFM_LE8(Char(Zero), Branch(Char(Zero), wz31, wz32, wz33, wz34), h) → new_foldFM_LE8(Char(Zero), wz33, h)
The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2, 3 >= 3
new_foldFM_LE8(Char(Zero), Branch(Char(Succ(wz3000)), wz31, wz32, wz33, wz34), h) → new_foldFM_LE8(Char(Zero), wz33, h)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3

foldFM_LE	k z fr EmptyFM	= foldFM_LE3 k z fr EmptyFM
foldFM_LE	k z fr (Branch key elt vw fm_l fm_r)	= foldFM_LE2 k z fr (Branch key elt vw fm_l fm_r)

foldFM_LE1	k z fr key elt vw fm_l fm_r True	= foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r
foldFM_LE1	k z fr key elt vw fm_l fm_r False	= foldFM_LE0 k z fr key elt vw fm_l fm_r otherwise